package jtg.generator;


import jtg.graphics.SootCFG;
import jtg.solver.Z3Solver;
import jtg.visualizer.Visualizer;
import soot.*;
import soot.jimple.InvokeExpr;
import soot.jimple.StaticFieldRef;
import soot.jimple.internal.*;
import soot.toolkits.graph.ClassicCompleteUnitGraph;
import soot.toolkits.graph.UnitGraph;
import soot.util.Chain;

import java.io.File;
import java.lang.reflect.Array;
import java.lang.reflect.Constructor;
import java.lang.reflect.Field;
import java.lang.reflect.Method;
import java.util.*;

public abstract class ParentGeneratorUitl {

    protected String clsPath;
    protected String clsName;
    protected String mtdName;
    ////这个方法的CFG
    protected UnitGraph ug;
    //方法的soot代码形式
    protected Body body;

    public int vCnt;
    public int eCnt;

    private int[][] edge;

    public List<Unit> vertexes;

    public List<Unit> heads;

    public List<Unit> tails;

    //private  boolean toTail;

    //protected int coverNodeCnt;
    //protected Set<Unit> coverNodeSet;
    protected static int LOOP_MAX_CNT_IN_EXTEND = 2;
    protected double coverRate;


    public ParentGeneratorUitl(String className, String methodName) {
        String defaultClsPath = System.getProperty("user.dir") + File.separator + "target" + File.separator + "classes";
        new SimpleGenerator(defaultClsPath, className, methodName);
    }

    public ParentGeneratorUitl(String classPath, String className, String methodName) {

        clsPath = classPath;
        clsName = className;
        mtdName = methodName;
        ug = SootCFG.getMethodCFG(clsPath, clsName, mtdName);
        body = SootCFG.getMethodBody(clsPath, clsName, mtdName);
        System.out.println("=============ug==============");
        System.out.println(ug);
        System.out.println("=============ug==============");
        System.out.println("=============boby==============");
        System.out.println(body);
        System.out.println("=============boby==============");

        stubInvoke();
        System.out.println("=============stubed boby==============");
        System.out.println(body);
        System.out.println("=============stubed boby==============");

//        drawCFG(methodName, false);

        vCnt = ug.size();
        vertexes = new ArrayList<>();
        heads = ug.getHeads();
        tails = ug.getTails();
        edge = new int[vCnt][vCnt];
        //coverNodeSet = new HashSet<>();
        for (Unit unit : ug) {
            vertexes.add(unit);
        }
        for (Unit unit : ug) {
            for (Unit nextToUnit : ug.getSuccsOf(unit)) {
                eCnt++;
                edge[vertexes.indexOf(unit)][vertexes.indexOf(nextToUnit)] = 1;
            }
        }

    }

    private int tmprId = 0;
    private int tmpiId = 0;

    private void mapper(HashMap<Value, Value> map, Value operator) {
        if (!map.containsKey(operator)) {
            JimpleLocal local;
            if (operator.toString().contains("r")) {
                local = new JimpleLocal("r_stub" + tmprId, operator.getType());
                tmprId++;
            } else {
                local = new JimpleLocal("i_stub" + tmpiId, operator.getType());
                tmprId++;
            }
            map.put(operator, local);
        }
    }

    private void stubInvoke() {
        UnitPatchingChain units = body.getUnits();
        Iterator<Unit> iterator = units.snapshotIterator();
        while (iterator.hasNext()) {
            Unit unit = iterator.next();

            if (unit instanceof JAssignStmt) {
                JAssignStmt assignStmt = (JAssignStmt) unit;
                if (assignStmt.containsInvokeExpr()) {
                    //left operator
                    Value leftOp = assignStmt.getLeftOp();
                    //right invokeExpr
                    InvokeExpr invokeExpr = assignStmt.getInvokeExpr();
                    //暂不支持静态调用
                    if (invokeExpr.toString().contains("staticinvoke")) continue;
                    List<Value> args = invokeExpr.getArgs();
                    System.out.println("invokeExpr: " + invokeExpr);
                    System.out.println("args: " + args);

                    //被调用方法的body
                    Body calledBody = (Body) invokeExpr.getMethod().retrieveActiveBody().clone();

                    //把calledBody的return语句变为赋值语句，把返回值赋给左操作数
                    UnitPatchingChain chain = calledBody.getUnits();
                    HashMap<Value, Value> map = new HashMap<>();
                    Iterator<Unit> unitIterator = chain.snapshotIterator();
                    while (unitIterator.hasNext()) {
                        Unit next = unitIterator.next();

                        if (next instanceof JReturnStmt) {
                            JReturnStmt stmt = (JReturnStmt) next;
                            Value op = stmt.getOp();
                            mapper(map, op);
                            stmt.setOp(map.get(op));
                            Value returnValue = stmt.getOp();
                            JAssignStmt temp = new JAssignStmt(leftOp, returnValue);
                            chain.insertBefore(temp, next);
                            chain.remove(next);
                        }

                        if (next instanceof JAssignStmt) {
                            JAssignStmt stmt = (JAssignStmt) next;
                            mapper(map, stmt.leftBox.getValue());
                            stmt.leftBox.setValue(map.get(stmt.leftBox.getValue()));
                            List<ValueBox> boxes = stmt.rightBox.getValue().getUseBoxes();
                            for (ValueBox box : boxes) {
                                if (map.get(box.getValue()) != null) //avoid replacing constant
                                    box.setValue(map.get(box.getValue()));
                            }
                        }

                        if (next instanceof JIdentityStmt) {
                            JIdentityStmt stmt = (JIdentityStmt) next;
                            mapper(map, stmt.leftBox.getValue());
                            Value newLeftValue = map.get(stmt.leftBox.getValue());
                            stmt.leftBox.setValue(newLeftValue);
                            String oriRightValueStr = stmt.rightBox.getValue().toString();
                            if (oriRightValueStr.contains("parameter")) {
                                oriRightValueStr = oriRightValueStr.replace("parameter", "");
                                int argIndex = Integer.parseInt(oriRightValueStr.substring(oriRightValueStr.indexOf("@") + 1, oriRightValueStr.indexOf(":")));
                                Value newRightValue = args.get(argIndex);
                                JAssignStmt temp = new JAssignStmt(newLeftValue, newRightValue);
                                chain.insertBefore(temp, next);
                                chain.remove(next);
                            }
                        }
                    }
                    units.insertOnEdge(chain, unit, null);
                    units.remove(unit);
                    ug = new ClassicCompleteUnitGraph(body);
                }
            }
        }
    }

    public void drawCFG(String graphName, boolean indexLabel) {
        Visualizer.printCFGDot(graphName, ug, indexLabel);
    }


    public abstract int coverNode(List<Unit> completePath);

    public abstract List<String> generate() throws Exception;

    public void dfsForAllPaths(Unit u, int[] visit, List<Unit> curPath, List<List<Unit>> targetPaths) {
        curPath.add(u);
        visit[vertexes.indexOf(u)]++;
        for (Unit v : ug.getSuccsOf(u)) {
            if (visit[vertexes.indexOf(v)] < LOOP_MAX_CNT_IN_EXTEND) {

                dfsForAllPaths(v, visit, curPath, targetPaths);

            } else {
                if (u instanceof JIfStmt)
                    continue;
                dfsForAllPaths(v, visit, curPath, targetPaths);

            }
        }
        for (Unit tail : tails) {
            if (u == tail) {
                ArrayList<Unit> units = new ArrayList<>(curPath);
                targetPaths.add(units);
                break;
            }
        }
        visit[vertexes.indexOf(u)] = 0;
        curPath.remove(curPath.size() - 1);

    }

    public List<List<Unit>> getAllCompeletePath() {
        ArrayList<Unit> curPath = new ArrayList<>();
        List<List<Unit>> targetPaths = new ArrayList<>();
        for (Unit head : heads) {
            dfsForAllPaths(head, new int[vCnt], curPath, targetPaths);
        }
        return targetPaths;
    }

    //以$开头的变量是Jvars
    protected List<Local> getJVars() {
        //Jimple自身增加的Locals，不是被测代码真正的变量
        ArrayList<Local> jimpleVars = new ArrayList<Local>();
        for (Local l : body.getLocals()) {
            if (l.toString().startsWith("$")) jimpleVars.add(l);
        }
        return jimpleVars;
    }

    //方法参数
    protected List<Local> getParameter() {
        ArrayList<Local> paras = new ArrayList<Local>();
        for (Local para : body.getParameterLocals()) {
            paras.add(para);
        }
        return paras;
    }


    protected String getTestStringFromTestObjects(List<Object> testObjects) {
        StringBuffer stringBuffer = new StringBuffer();
        List<Local> parameter = getParameter();
        for (int i = 0; i < parameter.size(); i++) {
            stringBuffer.append(parameter.get(i).getName());
            stringBuffer.append("=");
            if (parameter.get(i).getType().toString().contains("[]")) {
                if (parameter.get(i).getType().toString().contains("int[]"))
                    stringBuffer.append(Arrays.toString((int[]) testObjects.get(i)));
                else
                    stringBuffer.append(Arrays.toString((Object[]) testObjects.get(i)));

            } else {
                stringBuffer.append(testObjects.get(i).toString());
            }
            stringBuffer.append(" ");
        }

        return stringBuffer.toString();
    }


    protected Object getExpectedResult(List<Object> testObjects) {
        Class[] paraType = new Class[testObjects.size()];
        HashMap<Class, Class> baseClassMap = getObject2BaseClassMap();
        Object res = null;
        for (int i = 0; i < testObjects.size(); i++) {
            Class type = testObjects.get(i).getClass();
            paraType[i] = baseClassMap.get(type) != null ? baseClassMap.get(type) : type;
        }
        try {
            Class aClass = Class.forName(clsName);
            Object o = aClass.newInstance();
            res = aClass.getMethod(mtdName, paraType).invoke(o, testObjects.toArray());

        } catch (Exception e) {
            e.printStackTrace();
        }
        return res;

    }

    protected HashMap<Class, Class> getBase2ObjectClassMap() {
        HashMap<Class, Class> map = new HashMap<>();
        map.put(int.class, Integer.class);
        map.put(double.class, Double.class);
        map.put(short.class, Short.class);
        map.put(long.class, Long.class);
        map.put(boolean.class, Boolean.class);
        map.put(char.class, Character.class);
        return map;

    }

    protected HashMap<Class, Class> getObject2BaseClassMap() {
        HashMap<Class, Class> map = new HashMap<>();
        map.put(Integer.class, int.class);
        map.put(Double.class, double.class);
        map.put(Short.class, short.class);
        map.put(Long.class, long.class);
        map.put(Boolean.class, boolean.class);
        map.put(Character.class, char.class);
        map.put(Integer[].class, int[].class);
        map.put(Double[].class, double[].class);
        map.put(Short[].class, short[].class);
        map.put(Long[].class, long[].class);
        map.put(Boolean[].class, boolean[].class);
        return map;

    }

    //i0=0
    protected List<Object> getTestObjectsFromResString(String res) {
        List<Local> paras = getParameter();
        Class[] paraclasses = new Class[paras.size()];
        //测试输入参数
        Object[] parasObjects = new Object[paras.size()];
        //获取方法上的参数类型
        for (int i = 0; i < paras.size(); i++) {
            try {
                paraclasses[i] = getClassTypeFromSootType(paras.get(i).getType().toString());
            } catch (ClassNotFoundException e) {
                e.printStackTrace();
            }
        }

        // 获取具体的测试输入参数
        for (int i = 0; i < paras.size(); i++) {
            String sootParaName = paras.get(i).toString();
            List<String> assignAboutSootPara = new ArrayList<>();
            //获取关于该参数的赋值语句
            for (String s : res.split("\\s+")) {
                if (s.contains(sootParaName)) {
                    assignAboutSootPara.add(s);
                }
            }
            //如果没有关于该参数的赋值语句，那么该参数可以随机生成
            if (assignAboutSootPara.isEmpty()) {
                parasObjects[i] = getRadomObject(paras.get(i).getType().toString());
                continue;
            }

            try {
                parasObjects[i] = getObjectByCondition(paraclasses[i], assignAboutSootPara, i);
            } catch (ClassNotFoundException e) {
                throw new RuntimeException(e);
            }

        }


        return Arrays.asList(parasObjects);
    }

    /**
     * @param paraclass           参数类型
     * @param assignAboutSootPara 只包含关于这个参数的赋值语句
     * @return
     */
    protected Object getObjectByCondition(Class paraclass, List<String> assignAboutSootPara, int paraIndex) throws ClassNotFoundException {
        Object resObject = null;
        List<Class> baseType = Arrays.asList(new Class[]{Integer.class, Boolean.class, Short.class, Double.class, Long.class});
        if (baseType.contains(paraclass)) {
            //这种情况assignAboutSootPara只有一条
            Constructor<?> constructor = null;
            try {
                constructor = paraclass.getConstructor(String.class);
                String assign = assignAboutSootPara.get(0);
                assign = assign.substring(assign.indexOf("=") + 1);
                if (paraclass == Boolean.class) {
                    assign = "0".equals(assign) ? "false" : "true";
                }
                resObject = constructor.newInstance(assign);

            } catch (Exception e) {
                e.printStackTrace();
            }
            //todo

        } else if (paraclass == Character.class) {
            String assign = assignAboutSootPara.get(0);
            assign = assign.substring(assign.indexOf("=") + 1);
            resObject = (char) Integer.parseInt(assign);
        } else if (paraclass == String.class) {
            String assign = assignAboutSootPara.get(0);
            if (assign.contains("length")) {
                String slen = assign.substring(assign.indexOf("=") + 1);
                resObject = getRandomString(Integer.parseInt(slen));
            }
        } else if (paraclass == Array.class) {
            String assign = assignAboutSootPara.get(0);
            assign = assign.substring(assign.indexOf("=") + 1);
            String arrType = getParameter().get(paraIndex).getType().toString();
            arrType = arrType.substring(0, arrType.indexOf("["));
            if (arrType.contains("int")) {
                resObject = getRadomObject("int[]");
            } else {
                //Map<String,Class> baseString2baseMap =  getbaseString2baseClassMap();
                //Class<?> elType = baseString2baseMap.get(arrType)!=null?
                //        baseString2baseMap.get(arrType) : Class.forName(arrType);

                Object[] arrObjects = (Object[]) Array.newInstance(Class.forName(arrType), Integer.parseInt(assign));
                for (int i = 0; i < arrObjects.length; i++) {
                    arrObjects[i] = getRadomObject(arrType);
                }
                resObject = arrObjects;
            }


        } else if (paraclass.isEnum()) {
            String assign = assignAboutSootPara.get(0);
            int ordinal = Integer.parseInt(assign.substring(assign.indexOf("=") + 1));
            resObject = paraclass.getEnumConstants()[ordinal];

        } else {
            //    类的
            Object[] fieldValue = new Object[paraclass.getFields().length];
            Class[] fieldClass = new Class[paraclass.getFields().length];
            HashMap<Class, Class> base2ObjectMap = getBase2ObjectClassMap();
            for (int i = 0; i < paraclass.getFields().length; i++) {
                boolean hasAssignWithField = false;
                Class type = paraclass.getFields()[i].getType();
                fieldClass[i] = base2ObjectMap.get(type) != null ? base2ObjectMap.get(type) : type;
                try {
                    for (String assign : assignAboutSootPara) {
                        if (assign.contains(paraclass.getFields()[i].getName())) {
                            hasAssignWithField = true;
                            Constructor<?> constructor = fieldClass[i].getConstructor(String.class);
                            fieldValue[i] = constructor.newInstance(assign.substring(assign.indexOf("=") + 1));
                            break;
                        }
                    }
                } catch (Exception e) {
                    e.printStackTrace();
                }
                if (!hasAssignWithField) {
                    //    如果没有包含这个属性的值，那么就可以随机生成这个属性
                    fieldValue[i] = getRadomObject(paraclass.getFields()[i].getType().toString());
                }
            }

            try {
                resObject = paraclass.newInstance();
                Field[] fields = paraclass.getFields();
                for (int i = 0; i < fields.length; i++) {
                    fields[i].setAccessible(true);
                    fields[i].set(resObject, fieldValue[i]);
                }

            } catch (Exception e) {
                //throw new RuntimeException(e);
                e.printStackTrace();
            }


        }
        return resObject;
    }

    private Map<String, Class> getbaseString2baseClassMap() {
        HashMap<String, Class> map = new HashMap<>();
        map.put("int", Integer.class);
        map.put("double", Double.class);
        map.put("short", Short.class);
        map.put("long", Long.class);
        map.put("boolean", Boolean.class);
        //map.put()
        return map;

    }

    protected Class getClassTypeFromSootType(String sootType) throws ClassNotFoundException {
        if (sootType.equals("int")) {
            return Integer.class;
        } else if (sootType.equals("double")) {
            return Double.class;
        } else if (sootType.equals("long")) {
            return Long.class;
        } else if (sootType.equals("short")) {
            return Short.class;
        } else if (sootType.equals("boolean")) {
            return Boolean.class;
        } else if (sootType.equals("char")) {
            return Character.class;
        } else if (sootType.contains("[]")) {
            ///
            return Array.class;
        }
        //    复杂类型
        return Class.forName(sootType);
    }


    protected ArrayList<String> getExpectedResultSet(ArrayList<String> testSet) {
        ArrayList<String> expectedResult = new ArrayList<>();
        for (String testCase : testSet) {
            if ("".equals(testCase)) {
                expectedResult.add("无解");
            } else {
                expectedResult.add(getExpectedResult(testCase, getParameter()).toString());
            }
        }
        return expectedResult;
    }

    protected Object getExpectedResult(String testCase, List<Local> paras) {
        String[] input = testCase.split(" ");
        HashMap<String, String> testCaseMap = new HashMap<>();
        //Local[] paraArr = paras.toArray();
        Object[] inputParaValues = new Object[paras.size()];
        Class[] inputParaTypes = new Class[paras.size()];

        Object res = null;

        for (String s : input) {
            testCaseMap.put(s.substring(0, s.indexOf("=")), s.substring(s.indexOf("=") + 1));
        }


        for (int i = 0; i < paras.size(); i++) {
            if (paras.get(i).getType().toString().equals("int")) {
                inputParaValues[i] = Integer.parseInt(testCaseMap.get(paras.get(i).toString()));
                inputParaTypes[i] = int.class;
            } else if (paras.get(i).getType().toString().equals("double")) {
                inputParaValues[i] = Double.parseDouble(testCaseMap.get(paras.get(i).toString()));
                inputParaTypes[i] = double.class;
            } else if (paras.get(i).getType().toString().equals("boolean")) {
                inputParaValues[i] = Boolean.parseBoolean(testCaseMap.get(paras.get(i).toString()));
                inputParaTypes[i] = boolean.class;
            } else if (paras.get(i).getType().toString().equals("char")) {
                inputParaValues[i] = (testCaseMap.get(paras.get(i).toString()).charAt(0));
                inputParaTypes[i] = char.class;
            } else {
                //
                inputParaValues[i] = Integer.parseInt(testCaseMap.get(paras.get(i).toString()));
                try {
                    inputParaTypes[i] = Class.forName(paras.get(i).getType().toString());
                } catch (ClassNotFoundException e) {
                    throw new RuntimeException(e);
                }
            }

        }

        //     去调用方法走一遍
        try {

            //URL u = new URL("file:\\" + clsPath + "\\");
            //URLClassLoader loader = new URLClassLoader(new URL[]{u});
            Class<?> aClass = Class.forName(clsName);
            Object o = aClass.newInstance();
            Method method = aClass.getMethod(mtdName, inputParaTypes);
            res = method.invoke(o, inputParaValues);
        } catch (Exception e) {
            e.printStackTrace();
        }
        return res;


    }


    // 求出给定路径上个路径约束
    public String calPathConstraint(List<Unit> path) throws ClassNotFoundException {


        List<Local> jVars = getJVars();
        //真正代码中的局部变量
        List<Local> localVars = getLocalVars();

        List<Local> paraVars = getParameter();

        localVars.addAll(jVars);
        String pathConstraint = "";

        //key为变量名，var为赋值语句的右侧
        HashMap<String, String> assignList = new HashMap<>();
        ArrayList<String> stepConditionsWithJimpleVarsAndLocalVars = new ArrayList<String>();
        ArrayList<String> stepConditions = new ArrayList<String>();
        for (int i = 0; i < path.size(); i++) {
            Unit stmt = path.get(i);
            //JAssignment：是赋值语句
            if (stmt instanceof JAssignStmt) {
                String leftOp = ((JAssignStmt) stmt).getLeftOp().toString();
                String rightOp = ((JAssignStmt) stmt).getRightOp().toString();
                Value rightOp1 = ((JAssignStmt) stmt).getRightOp();

                if (leftOp.contains(".")) {
                    leftOp = leftOp.substring(0, leftOp.indexOf(".")) + "_" + leftOp.substring(leftOp.lastIndexOf(" ") + 1, leftOp.length() - 1);
                }
                if (rightOp.contains(".")) {
                    rightOp = rightOp.substring(0, rightOp.indexOf(".")) + "_" + rightOp.substring(rightOp.lastIndexOf(" ") + 1, rightOp.length() - 1);
                }
                if (leftOp.contains("length")) {
                    leftOp = leftOp.substring(leftOp.indexOf(" ") + 1, leftOp.indexOf("("));
                }
                //字符串的length
                if (rightOp.contains("length()")) {
                    rightOp = rightOp.substring(rightOp.indexOf(" ") + 1, rightOp.indexOf("("));
                }
                //i0 = lengthof r1数组
                if (rightOp.contains("lengthof")) {
                    rightOp = rightOp.substring(rightOp.indexOf(" ") + 1) + "_" + "length";
                }
                //数组
                if (rightOp.contains("[")) {
                    rightOp = rightOp.substring(0, 2) + "_" + rightOp.substring(rightOp.indexOf("[") + 1, (rightOp.indexOf("[") + 1 + 2));
                }
                //枚举
                if (rightOp1 instanceof StaticFieldRef) {
                    rightOp1 = (StaticFieldRef) rightOp1;
                    String rightOpStr = rightOp1.toString();
                    Class<?> aClass = Class.forName(rightOp1.getType().toString());
                    if (aClass.isEnum()) {
                        Class<Enum> enumClass = (Class<Enum>) aClass;
                        Enum[] enumConstants = enumClass.getEnumConstants();
                        for (Enum enumConstant : enumConstants) {
                            String name = enumConstant.name();
                            if (rightOpStr.contains(name)) {
                                rightOpStr = String.valueOf(enumConstant.ordinal());
                                break;
                            }

                        }
                        rightOp = rightOpStr;
                        //stepConditions.add();
                    }

                }

                for (Local paraVar : paraVars) {
                    if (rightOp.contains(paraVar.toString())) {
                        for (String key : assignList.keySet()) {
                            if (rightOp.contains(key)) {
                                rightOp = rightOp.replace(key, assignList.get(key));
                            }
                        }
                    }
                }
                for (Local localVar : localVars) {
                    if (rightOp.contains(localVar.toString()) && assignList.get(localVar.toString()) != null) {
                        rightOp = rightOp.replace(localVar.toString(), assignList.get(localVar.toString()));
                    }
                }
                assignList.put(leftOp, rightOp);
            }
            //是if语句
            else if (stmt instanceof JIfStmt) {
                String ifstms = ((JIfStmt) stmt).getCondition().toString();
                //有bug这样的nextUnit是path中第一个该stmt下一个节点
                //int nextUnitIndex = path.indexOf(stmt) + 1;
                //Unit nextUnit = path.get(nextUnitIndex);
                Unit nextUnit = path.get(i + 1);
                //如果ifstmt的后继语句不是ifstmt中goto语句，说明ifstmt中的条件为假
                if (!((JIfStmt) stmt).getTarget().equals(nextUnit))
                    ifstms = "!( " + ifstms + " )";
                else
                    ifstms = "( " + ifstms + " )";

                //替换条件里的局部变量
                for (Local localVar : localVars) {
                    if (ifstms.contains(localVar.toString()) && assignList.get(localVar.toString()) != null) {
                        ifstms = ifstms.replace(localVar.toString(), assignList.get(localVar.toString()));
                        //stopFlag= false;
                    }
                }
                stepConditions.add(ifstms);
            }
        }

        //检查是否有枚举类型参数中，如果有枚举类型，需要添加枚举的约束，让他不超过相关枚举的ordinal
        //检查是否有数组类型，数组类型的长度不能小于0
        //检查是否有String类型，他的长度不能小于0
        //检查是都是char类型，他的ascii不能小于0 不能大于127
        for (Local local : getParameter()) {
            String enumCstrnt = getEnumConstraints(local);
            String arrCstrnt = getArrayConstraints(local);
            String strCstrnt = getStringConstraints(local);
            String charSctrnt = getCharConstraints(local);
            if (!enumCstrnt.equals("")) {
                stepConditions.add(enumCstrnt);
            } else if (!arrCstrnt.equals("")) {
                stepConditions.add(arrCstrnt);
            } else if (!strCstrnt.equals("")) {
                stepConditions.add(strCstrnt);
            }
        }

        System.out.println("The step conditions with JimpleVarsAndLocalVars are: " + stepConditions);


        if (stepConditions.isEmpty())
            return "";

        //拼装路径上的约束( i0 % 15 != 0 ) && !( i0 % 5 != 0 )
        pathConstraint = stepConditions.get(0);
        int i = 1;
        while (i < stepConditions.size()) {
            pathConstraint = pathConstraint + " && " + stepConditions.get(i);
            i++;
        }


        return pathConstraint;
    }

    private String getCharConstraints(Local local) {
        String res = "";
        if (local.getType().toString().equals("char")) {
            res = String.format(" ( %s >= 0 ) && ( %s  <= 127)", local.getName(), local.getName());
        }
        return res;
    }

    private String getStringConstraints(Local local) {
        String res = "";
        if (local.getType().toString().equals("java.lang.String")) {
            res = String.format("( %s >= 0 ) ", local.getName() + "_length");
        }
        return res;
    }

    private String getArrayConstraints(Local local) {
        String res = "";
        //Type type = local.getType();
        if (local.getType() instanceof ArrayType) {
            res = String.format("( %s >= 0 ) ", local.getName() + "_length");
        }
        return res;
    }

    private String getEnumConstraints(Local local) throws ClassNotFoundException {
        String res = "";
        //Type type = local.getType();
        if (local.getType() instanceof RefType) {
            Class cls = Class.forName(local.getType().toString());
            if (cls.isEnum()) {
                int length = cls.getEnumConstants().length;
                res = String.format("( %s >= 0 ) && ( %s < %d )", local.getName(), local.getName(), length);
            }
        }
        return res;
    }

    protected List<Local> getLocalVars() {
        List<Local> jVars = getJVars();
        List<Local> parameter = getParameter();
        Chain<Local> locals = body.getLocals();
        List<Local> localVars = new ArrayList<>();
        for (Local local : locals) {
            if (jVars.contains(local))
                continue;
            if (parameter.contains(local))
                continue;
            localVars.add(local);
        }
        return localVars;
    }

    //根据路径约束求解来
    protected String solve(String pathConstraint) throws Exception {
        return Z3Solver.solve(pathConstraint);
    }

    //生成随机值
    protected String randomTC(List<Local> parameters) {

        String varName;
        String varValue = "";
        String testinput = "";

        for (Local para : parameters) {
            varName = para.getName();
            //System.out.println("randomTC: paraType："+ para.getType().toString());
            Object varobject = getRadomObject(para.getType().toString());
            if (varobject instanceof Object[])
                varValue = Arrays.toString((Object[]) varobject);
            else
                varValue = varobject.toString();

            //其它的基本类型没写
            testinput = testinput + " " + varName + "=" + varValue;
        }
        return testinput;
    }

    protected Object getRadomObject(String type) {
        //反射解析出来的类的类型名形如：class java.lang.String需要去除前面的class
        if (type.contains("class")) {
            type = type.substring(6);
        }
        Object res = null;
        if (type.equals("int")) {
            res = Integer.valueOf((int) (Math.random() * 100));
        } else if (type.equals("double")) {
            res = Double.valueOf((double) (Math.random() * 100));
        } else if (type.equals("long")) {
            res = Long.valueOf((long) (Math.random() * 100));
        } else if (type.equals("short")) {
            res = Short.valueOf((short) (Math.random() * 100));
        } else if (type.equals("char")) {
            res = Character.valueOf((char) getRandomString((int) (Math.random() * 100)).charAt(0));
        } else if (type.equals("boolean")) {
            res = true;
        } else if (type.equals("java.lang.String")) {
            res = (String) getRandomString((int) (Math.random() * 10));
        } else if (type.contains("int[]")) {
            //    形如int[] 说明是数组
            res = (int[]) getRandomArrInt(type.substring(0, type.indexOf("[]")), (int) (Math.random() * 10));
        } else {
            //类
            res = getRandomClass(type);
        }
        return res;
    }

    protected Object getRandomClass(String clsName) {
        //    更具类名获取CLass实例
        Object instance = null;
        try {
            Class aClass = Class.forName(clsName);
            Object[] enumConstants = aClass.getEnumConstants();
            if (enumConstants != null) {
                //    说明是枚举
                return enumConstants[(int) (Math.random() * enumConstants.length)];
            } else {
                //否则是类
                //    创建对应类型的实例
                instance = aClass.newInstance();
                //    给field赋值
                Field[] fields = aClass.getDeclaredFields();
                for (Field field : fields) {
                    field.setAccessible(true);
                    field.set(instance, getRadomObject(field.getType().toString()));
                }
            }

        } catch (ClassNotFoundException e) {
            System.err.println("没有该类，检查类名是否书写正确，" + clsName);
        } catch (InstantiationException e) {
            throw new RuntimeException(e);
        } catch (IllegalAccessException e) {
            throw new RuntimeException(e);
        }
        return instance;
    }

    protected int[] getRandomArrInt(String itemType, int arrLen) {
        int[] objects = new int[arrLen];
        for (int i = 0; i < objects.length; i++) {
            objects[i] = (Integer) getRadomObject(itemType);
        }
        return objects;

    }

    protected String getRandomString(int length) {
        String str = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789";
        Random random = new Random();
        StringBuffer stringBuffer = new StringBuffer();
        for (int i = 0; i < length; i++) {
            int strIndex = random.nextInt(62);
            stringBuffer.append(str.charAt(strIndex));
        }
        return stringBuffer.toString();

    }
}
